Concerning the security problem of local and global attacks on the Integrity Report Protocol (IRP), the StatVerif syntax was extended by adding constructors and destructors associated with the integrity measurement. The security of the Platform Configuration Attestation (PCA) was analyzed and the local and global attacks were found, including tampering the platform configuration register or revising stored measurement log by running unauthorized commands. The abilities of attackers were modeled, and how attackers accumulated knowledge and tampered PCA protocol by using constructors and destructors was introduced. Finally, the existence of attacking sequence was proved theoretically when PCA does not satisfy the correspondence property; and several propositions that PCA can meet the local reliability and gloabal reliability were given, which were proved by the formal verification tool Proverif.